COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	AXIOM
C00004 ENDMK
C⊗;
AXIOM
LET: LET1: S1=move(A,Table,S);
     LET2: S2=move(B,C,S1);
     LET3: S3=move(A,B,S2);;

DISTINCT: ¬(A=B),¬(A=C),¬(B=C),¬(A=Table),¬(B=Table),¬(C=Table);

UNIQUE: ∀x y z s.((¬(z=Table)∧(support(x,s)=z∧support(y,s)=z))⊃x=y);

TEST1: TEST11: support(A,S)=B;
       TEST12: support(B,S)=Table;
       TEST13: support(C,S)=Table;
       TEST14: clear(A,S);
       TEST15: clear(C,S);;

MOVE:
∀x y z s.(((y=Table∨clear(y,s))∧(clear(x,s)∧¬(z=x)))
      ⊃ support(z,move(x,y,s))=support(z,s)),

∀x y s.(((y=Table∨clear(y,s))∧clear(x,s))⊃y=support(x,move(x,y,s)));

CLEAR: ∀x s.(clear(x,s)≡∀z.¬(x=support(z,s)));  ;